(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun aa () Bool)
(declare-fun g () Bool)
(declare-fun h () Bool)
(declare-fun i () Bool)
(declare-fun j () Bool)
(declare-fun k () Bool)
(declare-fun l () Real)
(declare-fun n () Bool)
(declare-fun m () Bool)
(declare-fun ab () Bool)
(declare-fun q () Bool)
(declare-fun ac () Bool)
(declare-fun ad () Real)
(declare-fun o () Bool)
(declare-fun ae () Bool)
(declare-fun af () Bool)
(declare-fun r () Bool)
(declare-fun p () Bool)
(declare-fun s () Bool)
(declare-fun ag () Bool)
(declare-fun ah () Bool)
(declare-fun ai () Bool)
(declare-fun aj () Bool)
(declare-fun ak () Bool)
(declare-fun al () Bool)
(declare-fun am () Bool)
(declare-fun an () Bool)
(declare-fun ao () Real)
(declare-fun ap () Bool)
(declare-fun aq () Bool)
(declare-fun y () Bool)
(declare-fun ar () Bool)
(declare-fun t () Bool)
(declare-fun u () Bool)
(declare-fun v () Bool)
(declare-fun z () Bool)
(declare-fun x () Bool)
(declare-fun w () Bool)
(declare-fun bb () Bool)
(declare-fun bc () Bool)
(assert (or (= a 2.0) (= a 3.0 a 4.0)))
(assert (or (= b 1.0) (= b 2.0) (= b 3.0) (= b 4.0)))
(assert (or (= c 1.0) (= c 2.0 c 3.0) (= c 4.0)))
(assert (or (= d 1.0) (= d 2.0) (= 3.0 d 4.0)))
(assert (or (= 1.0 e 2.0) (= e 3.0) (= e 4.0)))
(assert (or (= f 1.0) (= f 2.0) (= f 3.0) (= f 4.0)))
(assert (= (= (+ (ite ac 1 0) (ite q 1 0) (ite m 1 0) (ite n 1 0)) 0) (= l 0.0)))
(assert (= ad 0.0))
(assert (<= (ite h 1 0) (ite aa 1 0)))
(assert (<= (+ (ite i 1 0) (ite k 1 0)) 1))
(assert (<= (+ (ite i 1 0) (ite j 1 0)) 10))
(assert (<= (+ (ite ab 1 0) (ite ac 1 0)) 1))
(assert (<= (+ (ite ab 1 0) (ite q 1 0)) 1))
(assert (<= (+ (ite ab 1 0) (ite n 1 0)) 1))
(assert (<= (+ (ite o 1 0) (ite ae 1 0)) (+ (ite r 1 0) (ite p 1 0)) 1))
(assert (<= (+ (ite aj 1 0) (ite ak 1 0)) 1))
(assert (<= (+ (ite aq 1 0) (ite aq 1 0) (ite y 1 0)) 1))
(assert (<= (+ (ite aq 1 0) (ite ap 1 0)) 1))
(assert (<= (+ (ite t 1 0) (ite v 1 0)) 1))
(assert (<= (+ (ite t 1 0) (ite u 1 0)) 0))
(assert (<= (+ (ite x 1 0) (ite z 1 0)) (+ (ite bb 1 0) (ite bc 1 0)) (ite w 1 0)))
(assert (<= (+ (ite g 1 0) (ite aa 1 0)) 1))
(assert (<= (+ (ite m 1 0) (ite n 1 0)) 1 (+ (ite af 1 0) 1) (ite p 1 0)))
(assert (<= (+ (ite ag 1 0) (ite s 1 0)) 1))
(assert (<= (+ (ite ai 1 0) (ite ah 1 0) (ite al 1 0)) (ite am 1 0) (ite an 1 0)))
(assert (<= (+ (ite ar 1 0) (ite v 1 0)) 1))
(check-sat)
